YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y)
  , %(0(), s(y)) -> 0()
  , %(s(x), s(y)) -> s(%(-(x, y), s(y))) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

We add following weak dependency pairs:

Strict DPs:
  { -^#(x, 0()) -> c_1(x)
  , -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , %^#(0(), s(y)) -> c_3()
  , %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { -^#(x, 0()) -> c_1(x)
  , -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , %^#(0(), s(y)) -> c_3()
  , %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }
Strict Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y)
  , %(0(), s(y)) -> 0()
  , %(s(x), s(y)) -> s(%(-(x, y), s(y))) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { -(x, 0()) -> x
    , -(s(x), s(y)) -> -(x, y) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { -^#(x, 0()) -> c_1(x)
  , -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , %^#(0(), s(y)) -> c_3()
  , %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }
Strict Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(c_2) = {1}, Uargs(%^#) = {1}, Uargs(c_4) = {1}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA) and not(IDA(1)).

            [0] = [0]
                  [0]
                     
    [-](x1, x2) = [1 0] x1 + [1]
                  [0 1]      [0]
                                
        [s](x1) = [1 0] x1 + [1]
                  [0 1]      [0]
                                
  [-^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
                  [1 2]      [1 2]      [2]
                                           
      [c_1](x1) = [0 0] x1 + [1]
                  [1 1]      [1]
                                
      [c_2](x1) = [1 0] x1 + [1]
                  [0 1]      [1]
                                
  [%^#](x1, x2) = [1 0] x1 + [0]
                  [0 0]      [0]
                                
          [c_3] = [1]
                  [1]
                     
      [c_4](x1) = [1 0] x1 + [1]
                  [0 1]      [2]

This order satisfies following ordering constraints


Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , %^#(0(), s(y)) -> c_3()
  , %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }
Weak DPs: { -^#(x, 0()) -> c_1(x) }
Weak Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 2: %^#(0(), s(y)) -> c_3()
  , 4: -^#(x, 0()) -> c_1(x) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_2) = {1}, Uargs(c_4) = {1}
  
  TcT has computed following constructor-restricted matrix
  interpretation. Note that the diagonal of the component-wise maxima
  of interpretation-entries (of constructors) contains no more than 0
  non-zero entries.
  
              [0] = [1]
                       
      [-](x1, x2) = [1] x2 + [1]
                                
          [s](x1) = [1]
                       
    [-^#](x1, x2) = [1]
                       
        [c_1](x1) = [0]
                       
        [c_2](x1) = [1] x1 + [0]
                                
    [%^#](x1, x2) = [1] x2 + [1]
                                
            [c_3] = [0]
                       
        [c_4](x1) = [1] x1 + [0]
  
  This order satisfies following ordering constraints
  
        [-^#(x, 0())] =  [1]                      
                      >  [0]                      
                      =  [c_1(x)]                 
                                                  
    [-^#(s(x), s(y))] =  [1]                      
                      >= [1]                      
                      =  [c_2(-^#(x, y))]         
                                                  
     [%^#(0(), s(y))] =  [2]                      
                      >  [0]                      
                      =  [c_3()]                  
                                                  
    [%^#(s(x), s(y))] =  [2]                      
                      >= [2]                      
                      =  [c_4(%^#(-(x, y), s(y)))]
                                                  

The strictly oriented rules are moved into the corresponding weak
component(s).

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }
Weak DPs:
  { -^#(x, 0()) -> c_1(x)
  , %^#(0(), s(y)) -> c_3() }
Weak Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ %^#(0(), s(y)) -> c_3() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }
Weak DPs: { -^#(x, 0()) -> c_1(x) }
Weak Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 1: -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , 2: %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y)))
  , 3: -^#(x, 0()) -> c_1(x) }
Trs: { -(s(x), s(y)) -> -(x, y) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_2) = {1}, Uargs(c_4) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
              [0] = [1]
                       
      [-](x1, x2) = [1] x1 + [0]
                                
          [s](x1) = [1] x1 + [1]
                                
    [-^#](x1, x2) = [1] x2 + [0]
                                
        [c_1](x1) = [0]
                       
        [c_2](x1) = [1] x1 + [0]
                                
    [%^#](x1, x2) = [1] x1 + [1]
                                
            [c_3] = [0]
                       
        [c_4](x1) = [1] x1 + [0]
  
  This order satisfies following ordering constraints
  
          [-(x, 0())] =  [1] x + [0]              
                      >= [1] x + [0]              
                      =  [x]                      
                                                  
      [-(s(x), s(y))] =  [1] x + [1]              
                      >  [1] x + [0]              
                      =  [-(x, y)]                
                                                  
        [-^#(x, 0())] =  [1]                      
                      >  [0]                      
                      =  [c_1(x)]                 
                                                  
    [-^#(s(x), s(y))] =  [1] y + [1]              
                      >  [1] y + [0]              
                      =  [c_2(-^#(x, y))]         
                                                  
    [%^#(s(x), s(y))] =  [1] x + [2]              
                      >  [1] x + [1]              
                      =  [c_4(%^#(-(x, y), s(y)))]
                                                  

The strictly oriented rules are moved into the corresponding weak
component(s).

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
  { -^#(x, 0()) -> c_1(x)
  , -^#(s(x), s(y)) -> c_2(-^#(x, y))
  , %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }
Weak Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ -^#(x, 0()) -> c_1(x)
, -^#(s(x), s(y)) -> c_2(-^#(x, y))
, %^#(s(x), s(y)) -> c_4(%^#(-(x, y), s(y))) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Wall-time: 0.377343s
CPU-time: 3.831417s

Hurray, we answered YES(O(1),O(n^1))